m:, n:{0..m}. upto(m)[n] = n   

latex

Definitions	x:A. B(x), , upto(n), t  T, A  B, A, P  Q, False, , S  T, Y, if b then t else f fi , tt, ff, i  j , {i..j}, P  Q, P  Q, i  j < k, P & Q, ||as||, t  ...$L, l[i], SQType(T), {T}, hd(l), nth_tl(n;as), i z j, b, i <z j, , Unit, Dec(P), P  Q,
Lemmas	nat wf, select wf, upto wf, le wf, int seg wf, length wf1, eq int wf, bool wf, iff transitivity, assert wf, eqtt to assert, assert of eq int, length wf2, bnot wf, not wf, eqff to assert, assert of bnot, not functionality wrt iff, decidable lt, nat properties, ge wf, select append front, length upto, select append back, length nil, length cons, non neg length